E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), pred?:(E(?E)),
p:(e:E, l:IdLnk.
p:(e':E
p:((e'':E. 
p:((rcv?(e''))
p:( (sender(e'') = e)
p:( (link(e'') = l)
p:( (((e'' = e')  e'' < e')  (loc(e') = destination(l)  Id)))),
e:E, l:IdLnk. sends-bound(p; e; l)  E 

latex

Definitions	x:A. B(x), x:A. B(x), P  Q, P  Q, P  Q, t  T, sends-bound(p; e; l), x. t(x), prop{i:l}, x(s)
Lemmas	pi1 wf, assert wf, rcv? wf, sender wf, IdLnk wf, link wf, cless wf, Id wf, loc wf, ldst wf, unit wf